\begin{tabbing}
$\forall$\=$E$:Type$_{\mbox{\scriptsize i}}$, $T$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$), ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), ${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)), ${\it when}$,\+
\\[0ex]${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$)).
\-\\[0ex]SESAxioms\{i:l\}($E$; $T$; ${\it pred?}$; ${\it info}$; ${\it when}$; ${\it after}$) $\in$ Prop$_{\mbox{\scriptsize i'}}$
\end{tabbing}